COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00004 ENDMK
C⊗;

1  ∃y.∀a.(aεy≡a⊂{b|¬(bεb)})    ∀E KPOWER {b|¬(bεb)}
2  ∀a.(aεy≡a⊂{b|¬(bεb)})  (2)  ∃E 1 (y)
3  {b|¬(bεb)}εy≡{b|¬(bεb)}⊂{b|¬(bεb)}  (2)  ∀E 2 {b|¬(bεb)}
4  {b|¬(bεb)}⊂{b|¬(bεb)}≡∀c.(cε{b|¬(bεb)}⊃cε{b|¬(bεb)})    ∀E SUBSET {b|¬(bεb)},{b|¬(bεb)}
5  cε{b|¬(bεb)}⊃cε{b|¬(bεb)}    TAUT cε{b|¬(bεb)}⊃cε{b|¬(bεb)} 
6  ∀c.(cε{b|¬(bεb)}⊃cε{b|¬(bεb)})    ∀I 5 c
7  {b|¬(bεb)}εy  (2)  TAUT {b|¬(bεb)}εy 3:4,6
8  ∃b.{b|¬(bεb)}εb    ∃I 7 y←b
9  SET({b|¬(bεb)})≡∃b.{b|¬(bεb)}εb    ∀E SET {b|¬(bεb)}
10  SET({b|¬(bεb)})    TAUT SET({b|¬(bεb)}) 8:9
11  ∀a.(aε{b|¬(bεb)}≡(SET(a)∧¬(aεa)))    ∧I KCOMP
12  {b|¬(bεb)}ε{b|¬(bεb)}≡(SET({b|¬(bεb)})∧¬({b|¬(bεb)}ε{b|¬(bεb)}))    ∀E 11 {b|¬(bεb)}
13  FALSE    TAUT FALSE 10,12